Journals
  Publication Years
  Keywords
Search within results Open Search
Please wait a minute...
For Selected: Toggle Thumbnails
Method of program path validation based on satisfiability modulo theory solver
REN Shengbing, WU Bin, ZHANG Jianwei, WANG Zhijian
Journal of Computer Applications    2016, 36 (10): 2806-2810.   DOI: 10.11772/j.issn.1001-9081.2016.10.2806
Abstract499)      PDF (797KB)(406)       Save
In programs, the path search space is too large because there are too many paths or complicated cycle paths, which directly affect the efficiency and accuracy for path validation. To resolve the above problem, a new program path validation method based on the Satisfiability Modulo Theory (SMT) solver was proposed. Firstly, loop invariants were extracted from the complicated cycle paths by using the method of decision tree, then the No-Loop Control Flow Graph (NLCFG) was constructed. Secondly, the information for basic paths was extracted via traversing Control Flow Graph (CFG) by using basic path method. Finally, the problem of path validation was converted into the problem of constraint solving by using a SMT solver as a constraint solver. Compared with CBMC and FSoft-SMT which were also based on SMT solver, the proposed method reduced validation time on test programs by more than 25% and 15% respectively. As for verification accuracy, the proposed method had significantly improvement. Experimental results show that this method can efficiently resolve the problem with too large path search space, and improve the efficiency and accuracy of path validation.
Reference | Related Articles | Metrics